da:k:Knd fp Type. Msg(da)  Type 

latex

Definitions	x:A. B(x), t  T, Msg(da), x. t(x), x(s)
Lemmas	Msg wf, fpf-cap wf, Knd wf, Kind-deq wf, rcv wf, Id wf, IdLnk wf, fpf wf